Code and Notes (Week 3 Thursday)

module PracticeWeekTwo where

import Test.QuickCheck
import Data.List.NonEmpty (group, NonEmpty, head)
import Data.Char
import Data.List (sort, sortOn)

-- these are the notes from today's practical class.
-- we skipped the induction section, as we covered it last week.
-- nevertheless, i will copy those notes here. If you want to 
-- see them being written, look for the recorded practical from 
-- week two.
{- INDUCTION QN
  goal: 
  map f (map g xs) = map (f . g) xs

  definition of map:
  map :: (a -> b) -> [a] -> [b]
  map _ []     = []                 -- eq 1
  map f (x:xs) = f x:map f xs       -- eq 2

  proof:

  proof by structural induction on the list xs.

  case for the empty list:
  map f (map g []) = map f ([]) -- eq 1
                   = map f []
                   = []
  map (f . g) [] = [] -- eq1
     base case proven!

  inductive case:
  map f (map g xs) = map (f . g) xs -- IH

  map f (map g (x:xs)) = map f (g x : map g xs) -- eq 2
                       = f (g x) : map f (map g xs) -- eq 2
                       = f (g x) : map (f . g) xs -- IH
                       = (f . g) x : map (f . g) xs
                       = map (f . g) (x:xs)
-}

-- the below was actually written during the practical in week 3.

data Natural = Zero
             | Succ Natural

-- q 1
toInt :: Natural -> Int
toInt Zero = 0
toInt (Succ n) = 1 + toInt n

-- q 2
instance Show Natural where
    show n = show $ toInt n

instance Eq Natural where
    Zero == Zero = True
    Succ n == Succ m = n == m
    Succ _ == Zero = False
    Zero == Succ _ = False

toNatural :: Int -> Natural
toNatural n | n<=0 = Zero
            | otherwise = Succ (toNatural (n-1))

instance Arbitrary Natural where
  arbitrary = (toNatural . getNonNegative) <$> arbitrary

natEqReflProp :: Natural -> Bool
natEqReflProp n = n == n

natEqTransProp :: Natural -> Natural -> Natural -> Property
natEqTransProp a b c = a == b ==> b == c ==> a == c


-- q3
{-
  we want to know that Eq is an equivalence relation.

  reflexivity means a == a
  transitivity means a == b /\ b == c ==> a == c 
  symmetry means a == b ==> b == a 

-}

-- q4

natPlus :: Natural -> Natural -> Natural
natPlus Zero m = m
natPlus (Succ n) m = Succ (natPlus n m)

natPlusSymmProp :: Natural -> Natural -> Bool
natPlusSymmProp a b = natPlus a b == natPlus b a

{-
  what will 2+0 look like?
  Succ (Succ Zero) + Zero
     = Succ (Succ Zero + Zero)
     = Succ (Succ (Zero + Zero))
     = Succ (Succ Zero)
-}

natMult :: Natural -> Natural -> Natural
natMult Zero m = Zero
natMult (Succ n) m = natPlus m (natMult n m)

natSub :: Natural -> Natural -> Natural
natSub n Zero = n
natSub Zero _ = Zero
natSub (Succ n) (Succ m) = natSub n m

-- q5
instance Ord Natural where
    compare Zero Zero = EQ
    compare Zero (Succ _) = LT
    compare (Succ _) Zero = GT
    compare (Succ n) (Succ m) = compare n m

{-
-- another approach using other stuff (this isn't the best solution)
instance Ord Natural where
    compare n m | n == m = EQ
                | natSub n m == Zero = LT
                | otherwise = GT
-}

-- monoids

-- a semigroup is
-- a type and a binary operation <>
-- that operation must be associative

-- a monoid is
-- a type and a bunary operation <>
-- AND an identity element
-- the operation is associative
-- we also have x <> id = x
--          and id <> x = x

{- q1 and q3
  LISTS can be a monoid
  ++ and []

  other ideas?
  zipplus:
  [1, 2, 3, 4, 5]
  [5, 4, 5]
  <>
  [6, 6, 8, 4, 5]
  id element: []

  zipplus':
  [1, 2, 3, 4, 5]
  [5, 4, 5]
  <>
  [6, 6, 8]
  id element: [0,0..]

  maxlength:
  id: []

  minlength:
  NOT A MONOID
-}


-- q2 (this was not covered in class - these are my notes nonetheless.
-- unfortunately there is no recording of me going through this work.
-- I hope my notes make sense to you!)
{- 2:
  Proofs about monoids.
  Set: lists
  Op: ++
  Id: []

  Associativity:
  for all x,y,z,
  x ++ (y ++ z) = (x ++ y) ++ z

  by induction on x:
  base case:
  [] ++ (y ++ z) = y ++ z
                 = ([] ++ y) ++ z

  inductive case:
  IH: x ++ (y ++ z) = (x ++ y) ++ z
  goal: (a:x) ++ (y ++ z) = ((a:x) ++ y) ++ z

  (a:x) ++ (y ++ z) = a:(x ++ (y ++ z)) -- definition of ++
                    = a:((x ++ y) ++ z) -- rewriting inductive hyp
                    = a:(x ++ y) ++ z   -- definition of ++
                    = ((a:x) ++ y) ++ z -- definition of ++
                    QED

  proof of (x ++ [] = x):
  by induction on x
  base case:
    ([] ++ [] = []) QED immediately
  inductive case:
    IH: x ++ [] = x
    goal: (a:x) ++ [] = a:x

    (a:x) ++ [] = a:(x ++ []) -- definition of ++
                = a:(x)       -- inductive hyp
                = a:x
                QED

  proof of ([] ++ x = x)
  no induction needed. provided directly from definition of ++
  [] ++ x = x 
          QED

 -}

-- parse, don't validate
-- word frequencies exercise

breakIntoWords :: String -> [String]
breakIntoWords = words

removePunctuation :: String -> String
removePunctuation s = filter (\x -> not (isPunctuation x)) s

sortStrings :: [String] -> [String]
sortStrings = sort

-- this is a this thing
-- [[this, this], [is]]

groupSame :: [String] -> [NonEmpty String]
groupSame = Data.List.NonEmpty.group

sortByLength :: [NonEmpty String] -> [String]
sortByLength ss = map Data.List.NonEmpty.head (reverse (sortOn length ss))

takeLongest :: Int -> [String] -> [String]
takeLongest = take

getReport :: String -> Int -> [String]
getReport s n = takeLongest n
              $ sortByLength
              $ groupSame
              $ sortStrings
              $ map removePunctuation
              $ breakIntoWords s